… toward #108)

The affine-accounting heart of ht_subst, all green under %default total:

  - combMaybe / uaddUSnocReduce / uaddSnocSplit  USnoc-tail uadd helpers
  - vecReassoc        lifts qReassoc to usage vectors (Maybe-equation form)
  - substReassocAdd   additive-split residual combine (uaddTotal + vecReassoc)
  - substReassocMult  multiplicative-split variant (q'=One)

Mirrors Coq vec_reassoc / subst_reassoc_add / subst_reassoc_mult. Refs #108

…, toward #108)

Completes the substitution accounting algebra, all green under %default total:

  - usplit3            USnoc-boundary usage split by length (drops unused
                       ulen-dg conjunct vs Coq usplit3)
  - uaddSplitBoundary2 USnoc-headed boundary sum split (heads add: q=q1+q2)
  - substVarSucc       deeper-index subst commutes with one weakening shift
                       (GT case needs minusZeroRight to bridge the stuck minus)

Mirrors Coq usplit3 / uadd_split_boundary2 / subst_var_succ. With A1+A2+A3
the full accounting layer beneath hvSubst/htSubst is done. Refs #108

…#108)

The variable case of the QTT substitution lemma (mirrors Coq hv_subst), green
under %default total. Prefix-I induction; matches n=Z/S n0 at runtime and
bridges varInv's erased witness via predEq'. Two leaves:
  - substituted variable itself  -> returns u, usage scaled by q (uaddZeroL)
  - any other variable           -> unchanged, Zero-scaled (uaddUscaleZeroR),
                                     re-weakened by htShift0 + substVarSucc

Refs #108

…5/R5b

First strand of the fundamentals -> implementation coupling (the path the user
chose). proofs/STATUS.md flags that the mechanised QTT core and the Rust
compiler are 'two disconnected universes': checker.rs is a conventional Hindley
checker with no usage/multiplicity axis. This new crate ports the
machine-checked usage-walk synthesiser into the compiler's own language:

  - Q semiring {0,1,ω} (qadd/qmul/qle) — Coq Quantity.v tables verbatim
  - usage vectors (uzero/onehot/uadd/uscale/ule) — Coq SoloCore.v
  - check : Tctx -> Tm -> Option<(Ty,Uvec)> — the one-pass synthesiser
    (SoloCore.v:2128), returning the type AND exact realised usage
  - aff_check — the affine-budget decision (aff_type_dec / aff_type_iff, R5b)

Faithful de Bruijn (snoc-list <-> Vec, innermost = last). 7 tests green,
incl. the 4 SoloCore.v 'reflexivity' Examples reproduced as oracle tests
(check_id_unit / drop_linear / dup_linear / dup_omega) + the R5b affine
discard — so the port is checked against the verified algorithm's own
closed computations. No external deps; cargo test -p my-qtt passes.

Next coupling step: elaborate the my-lang surface AST onto this core so the
running checker enforces the resource axis. Refs proofs/STATUS.md.